NoTerminationCheck4.agda:10,1-24
Termination checking pragmas can only precede a function definition
or a mutual block (that contains a function definition).
